A pipeline is a set of data processing elements connected in a series, where the output of one element is the input of the next one. Pipelining optimizes processor functionality by keeping all portions of the processor occupied, thus increasing the amount of useful work the processor can do in a given time. Pipelining typically reduces the processor's cycle time and increases the throughput (the number of instructions that can be executed in a unit of time, otherwise known as a clock cycle) of instructions. Elements of a pipeline are often executed in parallel to allow overlapping execution of multiple instructions with the same circuitry. Logic circuits are usually divided up into stages, including instruction decoding, arithmetic, and register fetching stages, wherein each stage processes one instruction at a time.
In microprocessors, achieving an efficient utilization of the execution units is a key factor in improving performance. However, maintaining uninterrupted flow of instruction is a challenge due to data and control dependencies between instructions of a program. Modern microprocessors employ aggressive optimizations trying to keep their execution units busy without violating inter-instruction dependencies. Such complex optimizations may cause subtle implementation bugs that can be hard to detect using conventional simulation-based verification techniques.
Formal verification is the act of using mathematical methods in proving or disproving the correctness of an implementation with respect to a certain specification, and a viable technique to cope with the increased complexity of hardware systems. In the context of hardware systems, the term implementation refers to a design description at any level of the hardware abstraction hierarchy, not only the final circuit layout. The term specification refers to the desired (correct) behavior of the design under consideration. Verification of these systems is done by providing a formal proof on an abstract mathematical model of the system, the correspondence between the mathematical model and the nature of the system being otherwise known by design.
The growth in complexity of hardware designs increases the importance of formal verification techniques in the hardware industry. This could be attributed to a greater need in the hardware industry, where errors can have devastating economic effects, to conclusively prove correctness of design architectures. Potential, subtle interactions between components make it increasingly difficult to exercise a realistic set of possibilities by simulation-based verification approaches. Formal verification can be helpful to conclusively prove correctness of systems by virtue of analysis of all the states, a coverage that is presently lacking in simulation-based approaches.